%!TEX root = paperEdit.tex
\section{Evaluation}
\label{sec:evaluation}

\subsection{Experimental Setting}

We have evaluated REPROVE using five commercially available
smart-cards. Our purpose was to assess REPROVE along
the following dimensions:
\begin{compactitem}
\item Functional success: the system infers at least one model. If
  REPROVE is unable to infer a model then, there are two cases:
  \begin{inparaenum}[(\itshape i\upshape)]
  \item the system has failed, or
  \item the communication is encrypted.
  \end{inparaenum}
  The latter case is not REPROVE's failure as it merely
  acts as a verification that the implementation is secure.
\item Quality of the results: the output captures at least a
  high-level view of the implementation. REPROVE can produce more than
  one output models. We consider the following outcomes to be of high
  quality:
  \begin{inparaenum}[(\itshape i\upshape)]
  \item a unique model which matches exactly both with the low- and
    the high-level views of the implementation, \ie the exchanged
    commands and the on-card executed operations, and
  \item two or more models that exactly match the high-level view of
    the implementation, \ie on-card executed operations.
  \end{inparaenum}
\end{compactitem}
\comment{To address these aspects we used the standard precision and
recall metrics, as defined by:}{introduced precision/recall evaluation
metric}
{\scriptsize
$$\textrm{precision} =\frac{\textrm{True
    Positives}}{\textrm{True Positives} + \textrm{False Positives}}, \quad
 \textrm{recall} = \frac{\textrm{True Postives}}{\textrm{True
     Positives} + \textrm{False Negatives}}$$
}
\noindent
where 
\begin{inparaenum}[(\itshape i\upshape)]
\item $\textrm{True Positive}$: the outcome model suggests the
  correct on-card operations and the exact meaning of the APDU trace,
\item $\textrm{False Positive}$: the outcome model suggests the
  correct on-card operations, and a inexact meaning of the APDU trace,
\item $\textrm{False Negative}$: the outcome model suggest incorrect
  on-card operations and a inexact meaning of the APDU trace.
\end{inparaenum}




For each smart-card we used the sniffed APDU trace as the input to
REPROVE. The trace was produced when the \func{C\_logIn} function was
called. We were aware of the implementation of each smart-card from
the beginning but we treated them as unknowns during the
reverse-engineering. We compared REPROVE's output with the actual
implementation. Because of a non-disclosure agreement we must refrain
from naming the cards and revealing details of the
reverse-engineering.


\subsection{Results}

%\subsubsection{Number of inferred models}


\stitle{Number of inferred models} REPROVE performed well in all cards
by inferring at least one model.
The results are presented in Table~\ref{log-in}. For Card$_3$,
Card$_4$ and Card$_5$ REPROVE inferred a unique model which matched
the actual implementation exactly. \comment{ For Card$_1$ and Card$_2$ REPROVE
suggested two models, with one matching the implementation exactly. In
both cases the exact on-card operations were identified, but addressed
different implementations.}{updated results based on optimised algorithm version 2}



%\begin{table}[!tb]

%\subsubsection{Security Vulnerabilities Suggested by the Models}
\stitle{Security Vulnerabilities Suggested by the Models} We evaluated
the possible attacks enabled by the smart-card vulnerabilities REPROVE
detected.
\begin{wraptable}[9]{r}{.4\linewidth}
  \centering 
\vspace{-5ex}
\begin{scriptsize}
  \begin{tabular}{  l | l|  l }
\textbf{Smart-card} & \textbf{Precision}  & \textbf{Recall} \\ \hline \hline
 %Aladdin eToken Pro
Card$_1$ & 0,5  & 1 \\
% Athena ASE Key USB
Card$_2$ & 0,5 & 1 \\
 % Siemens CardOS V3.4b 
Card$_3$ & 1 & 1  \\
%RSA SecureID 800 
 Card$_4$  & 1 & 1 \\
%Safesite Classic TPC IS V1 
 Card$_5$  & 1 & 1 
\end{tabular}
\end{scriptsize}
\vspace{-1ex}
  \caption{RSA PKCS\#11: \func{C\_logIn} function: reverse-engineering evaluation results.}
  \label{log-in}
%\end{table}
\end{wraptable}
%\paragraph{APDU Level} 
\begin{inparaenum}[(\itshape i\upshape)]
\item \textit{APDU Level.}
The first security vulnerability we
checked was sniffing the PIN. In all cases we
identified the authentication data that was used. In two
cards the PIN was sent in plain text which consequently allowed
man-in-the-middle attacks. For the remaining cards (and even
  though this is not in the context of this work) once the location of
  authentication data in the communication trace is determined one can
  try to use a brute-force attack to generate all potentially valid
  PINs and check whether this is enough to gain access. \\
%\paragraph{On-card operations} 
\item \textit{On-card operations.} The resulting models suggested the specific
  on-card operations that were executed during authentication with the
  token. Such knowledge may enable a blind-replay attack, where the
  attacker replays the exchanged data at specific points during
  communication; or, the attacker requests the same operations to be
  performed, in the hopes that these operations, albeit applied in a
  blind way, are enough to gain access to private and/or sensitive
  data. \\
%\paragraph{RSA PKCS\#11} 
\item \textit{RSA PKCS\#11.} We checked the resulting models for any incorrect
  use of the standard that may lead to security vulnerabilities. The
  specification of the RSA PKCS\#11 standard states that for each
  newly initiated session, session handles are produced to provide
  access to the token's objects \eg data, keys and certificates. The
  results obtained from REPROVE showed that none of the tested cards
  obeyed this. This departure from protocol may allow blind-replay of
  a given session. Instead, trivial methods for authentication are
  used. As the protocol is stateless, the same authentication methods
  are also used before all operations over sensitive data, meaning
  that insight into the \func{C\_logIn} function may also provide
  knowledge of the general authentication principles of the card.
\end{inparaenum}

\begin{wraptable}[8]{r}{0.6\linewidth}
  \centering
%  \vspace{-5ex}
  \begin{scriptsize}
  \begin{tabular}{ l| l| l| l| l| l   }
\textbf{Smart-card} & \textbf{Total B.CC} & \textbf{R.CC} & \textbf{R.SFC} & \textbf{R.FC}& \textbf{R.Model} \\
\hline \hline
Card$_1$ &  122 & 24 & 11 &3 & 2\\
Card$_2$ &  81881 & 12 & 4 &2& 2\\
Card$_3$ &  1 & 1 & 1 &1& 1\\
Card$_4$ &  1 & 1 & 1 &1& 1\\
Card$_5$ &  249 & 28 & 8 &3 & 1\\
\end{tabular}
\end{scriptsize}
\caption{Reduction in the number of alternative implementations
  during analysis.}
  \label{combinationsTable}
\end{wraptable}

\stitle{Narrowing-down the search space} The reverse-engineering of
proprietary APDUs is a combinatorial problem and the solution time
grows exponentially with the size of the APDU trace. REPROVE uses
search to advance towards the proof, and inference to block and
exclude directions from the search. During analysis the search space
is continuously restricted until the final model is produced.
\ncomment{To demonstrate REPROVE's effectiveness on that matter, we
  have implemented a baseline algorithm that generates a search tree
  that consists of all possible mappings (including different
  meanings of each command) of the APDU trace, based on the category
  each command belongs to. Table~\ref{combinationsTable} presents the
  command combinations produced by the baseline algorithm, termed
  \textit{B.CC}. The terms \textit{R.CC}, \textit{R.SBC} and \textit{R.FC}
  present REPROVE's total command, sub-functionality and functionality
  combinations respectively. \textit{Model} is the number of final model(s)
  suggested by REPROVE. At each successive step the number
  of alternative implementations is progressively reduced.}{new stuff
  here - wanted to demonstrate how well reprove restricts search
  space}


\begin{wraptable}[6]{r}{.65\linewidth}
  \centering 
\vspace{-5ex}
\begin{scriptsize}
  \begin{tabular}{  l | l|  l| l| l| l| l }
\textbf{Smart-card} & \textbf{Precision}  & \textbf{Recall} & \textbf{R.CC} & \textbf{R.SFC} & \textbf{R.FC} & \textbf{R.Model}\\ \hline \hline
 %Aladdin eToken Pro
Card$_1$ & 1  & 1 & 5 & 1 &2 &  1 \\
% Athena ASE Key USB
Card$_2$ & 1 & 1 & 512 &  69 &  8 & 1  \\

\end{tabular}
\end{scriptsize}
%\vspace{-1ex}
  \caption{RSA PKCS\#11: \func{C\_generateKey} function: reverse-engineering evaluation results.}
  \label{generate-key}
%\end{table}
\end{wraptable}

\stitle{Further Experiments} \ncomment{To test the generality of our
  methodology we conducted the same
  experiments for function \func{C\_generateKey} using the same cards
  as before. The generated trace of Card$_3$ and Card$\_5$ was
  encrypted, thus, the evaluation was impossible. For Card$\_4$
  REPROVE did not generated any model, as the implementation of the
  card did not conform to the standard. For the remaining two cards
  the results and the total number of produced combinations are shown
  in Table~\ref{generate-key}. For both cards REPROVE extracted a
  unique model which matched the actual implementation exactly.
}{generate-key: sinai arketa afta?}









\stitle{Discussion} \ncomment{ In all tested cases, REPROVE inferred
  at least a high-level model of the actual implementation. In some
  cases, the reverse-engineering outcome was more than one model. Each model
  captured the operations of the card but differed at the implementation
  level. We do not consider this as a failure since REPROVE provided
  at least a high-level view of the implementation. However, this
  shows the necessity of incorporating feedback techniques to refine
  the reverse-engineering outcome. A straightforward feedback
  technique is to send the analyzed commands to
  the card in order to check the validity of the results
  and discard suggestions that do not work. }{to allaksa ligo}




%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paperEdit"
%%% End: 
